\begin{tabbing}
ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$T$:Type\+
\\[0ex]$\times$${\it ks}$:(Knd List)
\\[0ex]$\times$$T$
\\[0ex]$\times$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow$$T$)
\\[0ex]$\times$($\mathbb{N}\rightarrow$$T$$\rightarrow\mathbb{B}$)
\\[0ex]$\times$($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$))
\\[0ex]$\times$($\mathbb{N}^{+}$ List)
\-
\end{tabbing}